Skip to content

[Merged by Bors] - chore(Algebra/Ring/CharZero): document scoped simp design choice#39262

Closed
Paul-Lez wants to merge 3 commits into
leanprover-community:masterfrom
Paul-Lez:remove-scoped-simps
Closed

[Merged by Bors] - chore(Algebra/Ring/CharZero): document scoped simp design choice#39262
Paul-Lez wants to merge 3 commits into
leanprover-community:masterfrom
Paul-Lez:remove-scoped-simps

Conversation

@Paul-Lez
Copy link
Copy Markdown
Collaborator

@Paul-Lez Paul-Lez commented May 12, 2026

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 12, 2026 •
edited
Loading

PR summary a4da030857

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 12, 2026
YaelDillies
YaelDillies reviewed May 12, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you find which PR introduced these tags?

@Paul-Lez
Copy link
Copy Markdown
Collaborator Author

Paul-Lez commented May 12, 2026

Can you find which PR introduced these tags?

I believe this PR: #15631.

@YaelDillies YaelDillies mentioned this pull request May 12, 2026
Closed
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented May 12, 2026

Maybe undo your change and turn this PR into an addition of a comment explaining the scoping

@Paul-Lez
Copy link
Copy Markdown
Collaborator Author

Paul-Lez commented May 12, 2026

Sounds good, will update this in a bit:)

@Paul-Lez Paul-Lez changed the title chore(Algebra/Ring/CharZero): remove scoped in simp attributes chore(Algebra/Ring/CharZero): document scoped simp design choice May 13, 2026
@Paul-Lez Paul-Lez requested a review from YaelDillies May 13, 2026 01:59
YaelDillies
YaelDillies approved these changes May 13, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer delegate

Comment thread Mathlib/Algebra/Ring/CharZero.lean Outdated
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 13, 2026

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 13, 2026
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented May 13, 2026

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 13, 2026

✌️ Paul-Lez can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 13, 2026
@Paul-Lez
Copy link
Copy Markdown
Collaborator Author

Paul-Lez commented May 13, 2026

bors merge

mathlib-bors Bot pushed a commit that referenced this pull request May 13, 2026
@Paul-Lez
chore(Algebra/Ring/CharZero): document scoped simp design choice (#…
bc03304 
…39262)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 13, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Algebra/Ring/CharZero): document scoped simp design choice [Merged by Bors] - chore(Algebra/Ring/CharZero): document scoped simp design choice May 13, 2026
@mathlib-bors mathlib-bors Bot closed this May 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Paul-Lez @YaelDillies @riccardobrasca